forall a: forall b:
forall Q:a->b:
I:a&Q;Q^ = I:a&Q;L:b,a